/*
 * Copyright (C) 2006 United States Government as represented by the
 * Administrator of the National Aeronautics and Space Administration (NASA).
 * All Rights Reserved.
 * 
 * This software is distributed under the NASA Open Source Agreement (NOSA),
 * version 1.3. The NOSA has been approved by the Open Source Initiative. See
 * the file NOSA-1.3-JPF at the top of the distribution directory tree for the
 * complete NOSA document.
 * 
 * THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY KIND,
 * EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT LIMITED TO, ANY
 * WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO SPECIFICATIONS, ANY
 * IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, OR
 * FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL BE
 * ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF PROVIDED, WILL CONFORM TO
 * THE SUBJECT SOFTWARE.
 */

package gov.nasa.jpf.symbc.probsym;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.search.*;
import gov.nasa.jpf.jvm.BooleanChoiceGenerator;
import gov.nasa.jpf.jvm.ChoiceGenerator;
import gov.nasa.jpf.jvm.DynamicElementInfo;
import gov.nasa.jpf.jvm.JVM;
import gov.nasa.jpf.jvm.MethodInfo;
import gov.nasa.jpf.jvm.ThreadInfo;
import gov.nasa.jpf.jvm.bytecode.Instruction;
import gov.nasa.jpf.jvm.bytecode.InvokeInstruction;
import gov.nasa.jpf.jvm.choice.IntIntervalGenerator;
import gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet;
import gov.nasa.jpf.symbc.SymbolicInstructionFactory;
import gov.nasa.jpf.symbc.heap.HeapChoiceGenerator;
import gov.nasa.jpf.symbc.modelcounter.ModelCounter;
import gov.nasa.jpf.symbc.numeric.Constraint;
import gov.nasa.jpf.symbc.numeric.DependencyCalc;
import gov.nasa.jpf.symbc.numeric.PCChoiceGenerator;
import gov.nasa.jpf.symbc.numeric.PathCondition;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.logging.FileHandler;
import java.util.logging.SimpleFormatter;

import org.apfloat.Apfloat;
import org.apfloat.Apint;


/**
 * Listener that implements probabilistic symbolic execution.
 * 
 * @author Willem Visser
 * @author Jaco Geldenhuys
 */
public class ProbSymListener extends ListenerAdapter {

	/**
	 * The model counters invoked to calculate path probabilities. Only the
	 * first model counter's results are really taken into account; the others
	 * are merely there for experimental comparisons.
	 */
	private List<ModelCounter> modelCounters = null;

	/**
	 * The total number of constraints that appears in the path conditions
	 * processed.
	 */
	private int totalConstraints = 0;

	/**
	 * The total number of constraints that appears in the minimal path
	 * conditions produced.
	 */
	private int totalMinConstraints = 0;

	/**
	 * Mapping from path conditions to the conditional probability of the last
	 * ("freshest") constraint of each path condition.
	 */
	private Map<PathCondition, Apfloat> conditionalMap;

	/**
	 * The previous minimal path condition produced.
	 */
	private PathCondition minimalPC = null;

	/**
	 * The path probability of the current, minimal path condition excluding the
	 * freshest constraint.
	 */
	private Apfloat prior = Apfloat.ZERO;

	/**
	 * Caches (one per model counter) for memoization of calls.
	 */
	private Map<ModelCounter, Map<PathCondition, Apfloat>> cache;

	
	/*
	 * APfloat precision is set here
	 */
	private static final int PRECISION = 500;
	
	
	/**
	 * Logging
	 */
	
	static private FileHandler fileTxt;
	static private SimpleFormatter formatterTxt;
	
	/*
	private final static Logger LOGGER = Logger.getLogger(ProbSymListener.class
			.getName());
*/
	/*
	 * Coverage Data
	 */
	/*
	 * Maps Coverage to the Maximum probability of reaching that coverage
	 */
	private Map<Integer,Map<String,Apfloat>> covData = new HashMap<Integer,Map<String,Apfloat>>();
	//private Map<Integer,Map<PathCondition,Apfloat>> covData = new HashMap<Integer,Map<PathCondition,Apfloat>>();
	/*
	 * Maps PathCondition to Path Probabilities
	 */
	//private Map<PathCondition,Apfloat> pathProbMap = new HashMap<PathCondition,Apfloat>();
	private Map<String,Apfloat> pathProbMap = new HashMap<String,Apfloat>();
	/**
	 * Last instance of the listener created so that we can invoke it from a static routine.
	 */
	private static ProbSymListener instance;

	/*
	 * Null Probability in Heap Choices
	 */
	
	private static Apfloat nullProb = Apfloat.ONE.divide(new Apfloat(5,PRECISION)); // 20%
	
	/*
	 * Null Probability in Heap Choices
	 */
	
	private static Apfloat newProb = Apfloat.ONE.multiply(new Apfloat(7,PRECISION)).divide(new Apfloat(10,PRECISION)); // 70%
	
	
	
	/*
	 * Debug flag
	 */
	public boolean debugMode = false;
	
	/**
	 * Constructor.
	 * 
	 * @param conf
	 *            JPF configuration file
	 */
	public ProbSymListener(Config conf) {
		instance = this;
		
		String[] dummy = conf.getStringArray("probsym.debug");
		if (dummy != null) {
			debugMode = true;
		} else {
			debugMode = false;
		}
		
		modelCounters = conf.getInstances("symbolic.prob_modelcounter",
				ModelCounter.class, new Class[] { Config.class },
				new Object[] { conf });
		cache = new HashMap<ModelCounter, Map<PathCondition, Apfloat>>();
		if ((modelCounters == null) || modelCounters.isEmpty()) {
			modelCounters = new ArrayList<ModelCounter>();
			System.out.println("symbolic.prob_modelcounter=<<NONE SPECIFIED>>");
		} else {
			for (ModelCounter m : modelCounters) {
				System.out.println("symbolic.prob_modelcounter="
						+ m.getClass().getName());
				cache.put(m, new HashMap<PathCondition, Apfloat>());
			}
		}
		
		conditionalMap = new HashMap<PathCondition, Apfloat>();
	/*
		Logger logger = Logger.getLogger("");
		logger.setLevel(Level.INFO);
		try {
			fileTxt = new FileHandler("Logging.txt");
		} catch (IOException e) {
			e.printStackTrace();
		}
		formatterTxt = new SimpleFormatter();
		fileTxt.setFormatter(formatterTxt);
		LOGGER.addHandler(fileTxt);
		LOGGER.setLevel(Level.INFO);
		LOGGER.info("Welcome to SymbolicListener Logging");
		*/
	}

	
	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * gov.nasa.jpf.ListenerAdapter#instructionExecuted(gov.nasa.jpf.jvm.JVM)
	 */
	@Override
	public void instructionExecuted(JVM vm) {
		Instruction insn = vm.getLastInstruction();
		if (insn instanceof InvokeInstruction) {
			InvokeInstruction call = (InvokeInstruction) insn;
			ThreadInfo ti = vm.getLastThreadInfo();
			MethodInfo mi = call.getInvokedMethod(ti);
			if (mi != null) {
				String mthName = mi.getFullName();
				if (mthName
						.equals("gov.nasa.jpf.symbc.probsym.Analyze.coverage(Ljava/lang/String;)V")) {
					handleCoverage(call, vm);
				}
			}
		}
	}
	class ProbReturn {
		String desc;
		Apfloat prop;
		public ProbReturn(String d, Apfloat p) {
			desc = d;
			prop = p;
		}
	}

	private ProbReturn doUniversalProbCalc(ChoiceGenerator<?> cg) {
		Apfloat pr = new Apfloat(1.0,PRECISION);
		Apfloat p;
		String desc = "";
		while (cg != null) {
			if (cg instanceof PCChoiceGenerator) {
				PathCondition pc =  ((PCChoiceGenerator) cg).getCurrentPC();
				if (debugMode) {
					System.out.println("Found PC CG " + (PCChoiceGenerator)cg);
					System.out.println("PC = " + pc);
				}
				p = conditionalMap.get(pc);
				if (p == null) {
					if (debugMode)
						System.out.println("prob not found in store ");	
					if (pc == null) {
						if (debugMode)
							System.out.println("!!!pc is null!!!!");
						p = Apfloat.ONE;
					} else {					
						p = calcProbability(pc);
					}
				}
				else {
					if (debugMode)
						System.out.println("from store prob = " + p);					
				}
				if (!desc.contains(""+pc.header)) {
					if (debugMode) {
						System.out.println("desc so far " + desc);
						System.out.println("ppc = " + pc.header);
					}
					desc += pc.header;
				}
				pr = pr.multiply(p);
			}
			else if (cg instanceof HeapChoiceGenerator) {				
				HeapChoiceGenerator hcg = (HeapChoiceGenerator)cg;
				int choices = hcg.getTotalNumberOfChoices();
				int currentChoice = hcg.getNextChoice();
				if (choices == 2) { // only null and new, then use newProb=1-nullProb 
					if (currentChoice == 0) {
						p = nullProb;
					} else { // currentChoice == 1
						p = Apfloat.ONE.subtract(nullProb);
					}
				} else if (choices > 2) {
					if (currentChoice == 0) {
						p = nullProb;
					} else if (currentChoice == 1){
						p = newProb;
					} else { // 2 or more
						Apfloat aliasProb = Apfloat.ONE.subtract(nullProb).subtract(newProb);
						p = aliasProb.divide(new Apfloat(choices - 2,PRECISION));
					}
					
				} else {
					p = Apfloat.ONE.divide(new Apfloat(choices, PRECISION));
				}
				if (debugMode) {
					System.out.println("Found  Heap CG " + (HeapChoiceGenerator)cg);
					System.out.println("prop (" + choices + ") = " + p);
				}
				pr = pr.multiply(p);
				desc += hcg;
			}
			else if (cg instanceof IntIntervalGenerator) {
				int choices = cg.getTotalNumberOfChoices();
				p = Apfloat.ONE.divide(new Apfloat(choices, PRECISION)); 
				if (debugMode) {
					System.out.println("Found Int CG " + (IntIntervalGenerator)cg);
					System.out.println("prop (" + choices + ") = " + p);
				}
				pr = pr.multiply(p);
				desc += (IntIntervalGenerator)cg;
			}
			else if (cg instanceof ThreadChoiceFromSet) {
				int choices = cg.getTotalNumberOfChoices();
				p = Apfloat.ONE.divide(new Apfloat(choices, PRECISION)); 
				if (debugMode) {
					System.out.println("Found Scheduling CG " + (ThreadChoiceFromSet)cg);
					System.out.println("prop (" + choices + ") = " + p);
				}
				pr = pr.multiply(p);
				desc += (ThreadChoiceFromSet)cg;
			}
			else if (cg instanceof BooleanChoiceGenerator) {
				
				int choices = cg.getTotalNumberOfChoices();
				p = Apfloat.ONE.divide(new Apfloat(choices, PRECISION)); 
				if (debugMode) {
					System.out.println("Found Boolean CG " + (BooleanChoiceGenerator)cg);
					System.out.println("prop (" + choices + ") = " + p);
				}
				pr = pr.multiply(p);
				desc += (BooleanChoiceGenerator)cg;
			}
			else {
				System.out.println("Cannot Calculate Probability: Found unknown CG " + cg);
			}
			cg = cg.getPreviousChoiceGenerator();
		}
		if (debugMode) {
			System.out.println("Description = " + desc);
			System.out.println("Final probability = " + String.format("%.10s", pr));
		}
		return new ProbReturn(desc,pr);
	}
	/**
	 * Intercept calls to
	 * {@link gov.nasa.jpf.symbc.probsym.Analyze#coverage(String)} and record
	 * information about the current path probability.
	 * 
	 * @param call
	 *            the instruction that caused this method to be called
	 * @param vm
	 *            the JPF Java virtual machine
	 */

	public void handleCoverage(InvokeInstruction call, JVM vm) {
		DynamicElementInfo ei = (DynamicElementInfo) call.getArgumentValue("s",
				vm.getLastThreadInfo());
		
		ProbReturn ret = doUniversalProbCalc(vm.getChoiceGenerator());
		Apfloat pr = ret.prop;
		String pathDescription = ret.desc;
		assert pr.compareTo(Apfloat.ZERO) >=0;
		
		assert pr.compareTo(Apfloat.ONE) <= 0;
		
		Apfloat tmpVal = pathProbMap.get(pathDescription);
		if (tmpVal != null) {
			if (tmpVal.compareTo(pr) > 0)
				pr = tmpVal; // just keep the max prob for each location
		}	
		if (debugMode)
			System.out.println("Path = " + pathDescription + " prb = " + String.format("%.10s", pr));
		pathProbMap.put(pathDescription, pr);		
		
		int loc = Integer.parseInt(ei.asString());
		Map<String,Apfloat> covList = covData.get(loc);
		if (covList == null) {
			covList = new HashMap<String,Apfloat>();
		}
		covList.put(pathDescription,pr);
		covData.put(loc, covList);
		
		
		/* old working version
		PathCondition pc = PathCondition.getPC(vm);
		if (pc == null)
			return;
		pc = PathCondition.getPC(vm).make_copy(); 
		PathCondition orig = pc.make_copy();
		Apfloat pr = new Apfloat(1.0,PRECISION);
		pr = calcProbability(orig);
		pc.removeHeader(); // we assume that header's conditional probability is calculated by now
		while (pc.header != null) {
			pr = pr.multiply(conditionalMap.get(pc));
			
			System.out.println("PC pr = " + String.format("%.10s", pr) + " -> " + String.format("%.10s", conditionalMap.get(pc)));
			pc.removeHeader();
		}
		
		//System.out.println("res = " + String.format("%.10s", res) + " pr = " + String.format("%.10s", pr) + " diff = " + String.format("%.10s", res.subtract(pr)));
		
				
		
		LOGGER.info(ei.asString() + "  PathProb = " + pr + " for PC " + orig);
		
		assert pr.compareTo(Apfloat.ZERO) >=0;
		
		assert pr.compareTo(Apfloat.ONE) <= 0;
		
		PathCondition storePC = orig;//calcMinPCOnly(orig); 
		Apfloat tmpVal = pathProbMap.get(storePC);
		if (tmpVal != null) {
			//System.out.println("Loc " + ei.asString() + " compare " + tmpVal.compareTo(pr) + " Found old value " + tmpVal + " and new val is " + pr);
			//assert tmpVal.compareTo(pr) == 0;
			if (tmpVal.compareTo(pr) > 0)
				pr = tmpVal; // just keep the max prob for each location
		}		
		System.out.println("STOREPC = " + storePC + " prb = " + String.format("%.10s", pr));
		pathProbMap.put(storePC, pr);
		
		//pathProbMap.put(minimalPC, pr);
		
		//System.out.println(ei.asString() + "  PathProb = " + pr + " for PC " + orig);
		
		int loc = Integer.parseInt(ei.asString());
		Map<String,Apfloat> covList = covData.get(loc);
		if (covList == null) {
			covList = new HashMap<String,Apfloat>();
		}
		covList.put(storePC,pr);
		covData.put(loc, covList);
		*/
	}
	
	private static final Apfloat MILLION = new Apfloat(1000000,PRECISION);
	
	private Apfloat calcProbability(PathCondition pc) {
		Apfloat p = conditionalMap.get(pc);
		if (p != null) {
			//already did this one before
			return p;
		}
		if (pc != null) {
			//System.out.println("$$ org: " + pc);
			calcMinPC(pc); 
			//System.out.println("$$ min: " + minimalPC);
			totalConstraints += pc.count();
			totalMinConstraints += minimalPC.count();
//			double r = minimalPC.count() / (double) pc.count();
			//System.out.println("Reduction = " + r + " " + minimalPC.count()
			//		+ " " + pc.count());
			p = getConditionalProbability(minimalPC, prior);
			//System.out.println("Total = " + total + " current " + (finish-start) + " size = " + minimalPC.count()) ;
			conditionalMap.put(pc, p);			
			// now add the 1-p probability for the other branch to the conditionalMap
			Constraint negHead = pc.header.not();
			PathCondition notPC = pc.make_copy();
			notPC.removeHeader();
			notPC.prependUnlessRepeated(negHead);				
			conditionalMap.put(notPC, Apfloat.ONE.subtract(p));
		}
		return p;
	}

	public Apfloat calculateProbability2(PathCondition pc) {
		PathCondition c = pc.make_copy();
		c.removeHeader();
		Apfloat p = Apfloat.ONE;
		while (c.header != null) {
			p = p.multiply(conditionalMap.get(c));
			c.removeHeader();
		}
		return p;
	}

	public static Apfloat calculateProbability(PathCondition pc) {
		return instance.calculateProbability2(pc);
	}
	
	Apfloat totalViolationProb = new Apfloat(0.0);
	@Override
	public void propertyViolated(Search search) {		
		ProbReturn ret = doUniversalProbCalc(search.getVM().getChoiceGenerator());
		if (debugMode) {
			System.out.println("Path Desc" + ret.desc);
			System.out.println("prob = " + String.format("%.10s", ret.prop));
		}
		totalViolationProb = totalViolationProb.add(ret.prop);
	}
	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * gov.nasa.jpf.ListenerAdapter#stateAdvanced(gov.nasa.jpf.search.Search)
	 */
	@Override
	public void stateAdvanced(Search search) {
		PathCondition pc = getPC(search.getVM());
		if (pc != null) {
			ProbReturn ret = doUniversalProbCalc(search.getVM().getChoiceGenerator());
			Apfloat pr = ret.prop;
			assert pr != null; // probably redundant
			if (search instanceof ProbHeuristic) {
				ProbHeuristic s = (ProbHeuristic) search;
				s.probHeuristicValue = pr.multiply(MILLION).intValue();
				// smaller values == higher priority
				System.out.println("Heuristic Prob value  = "
						+ s.probHeuristicValue);
			}
		}
	}

	private Apfloat getConditionalProbability(PathCondition minimalPC,
			Apfloat prior) {
		Apfloat pr = new Apfloat(0.5, PRECISION); // default guess
		for (ModelCounter m : modelCounters) {
			Map<PathCondition, Apfloat> c = cache.get(m);
//			String x = minimalPC.toString().replaceAll("\n", " ").replaceAll("_[0-9][0-9]*_SYMINT", "").replaceAll("CONST_", "");
			if (!c.containsKey(minimalPC)) {
				pr = m.getConditionalProbability(minimalPC, prior);
				c.put(minimalPC, pr);
				//System.out.println(m.getClass().getName() + "::Prob(PC) = "
				//		+ pr);
			} else {
				pr = c.get(minimalPC);
			}
		}
		return pr;
	}

	static int printCount = 0;
	@Override
	public void stateBacktracked(Search search){
		//if (printCount++ % 50 == 0)
		//searchFinished(search);
	}
	/*
	 * (non-Javadoc)
	 * 
	 * @see
	 * gov.nasa.jpf.ListenerAdapter#searchFinished(gov.nasa.jpf.search.Search)
	 */
	@Override
	public void searchFinished(Search s) {
		SymbolicInstructionFactory.solver.shutdown();
		for (String str : SymbolicInstructionFactory.solver.getSolverReport()) {
			System.out.println(str);
		}
		if (modelCounters.size() == 0)
			return;
		for (ModelCounter m : modelCounters) {
			m.report();
		}
		//ModelCounter latte = modelCounters.get(0);
		Map<String,LinkedList<Integer>> pcToCoverageMap = new HashMap<String,LinkedList<Integer>>();
		for (Map.Entry<Integer,Map<String,Apfloat>> e : covData.entrySet()) {
			Apfloat maxProb = new Apfloat(0.0,PRECISION);
			Apfloat minProb = new Apfloat(1.0, PRECISION);
			
			String pcForMax = null;
			String pcForMin = null;
			
			Apfloat sum = new Apfloat(0.0,PRECISION);
			Set<String> setPC = new HashSet<String>();
			for(Map.Entry<String,Apfloat> pcProbMap : e.getValue().entrySet()) {
				String pathCond = pcProbMap.getKey();
				LinkedList<Integer> covList = pcToCoverageMap.get(pathCond);
				if (covList == null)
					covList = new LinkedList<Integer>();
				covList.add(e.getKey());
				pcToCoverageMap.put(pathCond, covList);
				Apfloat a = pcProbMap.getValue();
				sum = sum.add(a);
				if (a.compareTo(maxProb) > 0) {
					maxProb = a;
					pcForMax = pcProbMap.getKey();
				}
				if (a.compareTo(minProb) <= 0) {
					minProb = a;
					pcForMin = pcProbMap.getKey();
				}
				setPC.add(pathCond);
				//totalProb = totalProb.add(a);
			}
			//System.out.println(e.getKey() + " PCs =  " + setPC);
			//this only works for LattE now
			Apfloat res = new Apfloat(0.0, PRECISION);
			int times = e.getValue().size();			
//			if (times <= 9 && latte instanceof LattECounter) {				
//				//res = latte.getProbability(setPC);
//			}
			Apfloat minBound = minProb.multiply(new Apfloat(times-1, PRECISION)).add(maxProb);
			//System.out.println("For these disjuncts " + setPC + " we get combined = " + res);
			System.out.println("Location " + e.getKey() + " Times " + times + 
							   " max " + String.format("%.30s", maxProb) +
							   " min " + String.format("%.30s", minProb) +
							   " lower " + String.format("%.30s", minBound) +
							   " total all paths " + String.format("%.30s", res) +
							   " sum all paths " + String.format("%.30s", sum)
							   //" total " + String.format("%.10s", totalProb) 
							   //+ " PC " + pcForMax
							   );
		}
		Apfloat minProb = new Apfloat(1.0,PRECISION);
		Set<String> sameUnlikely = new HashSet<String>();
		for (Map.Entry<String, LinkedList<Integer>> e : pcToCoverageMap.entrySet()) {
			Apfloat tmp = pathProbMap.get(e.getKey());
			//System.out.println("PC = " + e.getKey() + " Prob = " + tmp);
			//for (Integer i : e.getValue()) {
			//	System.out.print(" " + i);
			//}			
			
			if (minProb.compareTo(tmp) > 0) {
				minProb = tmp;
				sameUnlikely.clear();
				sameUnlikely.add(e.getKey());
			}
			else if (minProb.compareTo(tmp) == 0) {
				sameUnlikely.add(e.getKey());
			}
			
		}
		System.out.println("\n Most Unlikely Paths with prob "+ String.format("%.10s", minProb) + " " + sameUnlikely);
		System.out.println("Violation prob " + String.format("%.10s",totalViolationProb));		
	}

	/**
	 * Find and return the path condition for the current state.
	 * 
	 * @param vm
	 *            the current JPF virtual machine
	 * @return the path condition
	 */
	private static PathCondition getPC(JVM vm) {
		// OLD CODE
		// ChoiceGenerator<?> cg = vm.getChoiceGenerator();
		// PathCondition pc = null;
		//
		// if (!(cg instanceof PCChoiceGenerator)) {
		// ChoiceGenerator<?> prev_cg = cg.getPreviousChoiceGenerator();
		// while (!((prev_cg == null) || (prev_cg instanceof
		// PCChoiceGenerator))) {
		// prev_cg = prev_cg.getPreviousChoiceGenerator();
		// }
		// cg = prev_cg;
		// }
		//
		// if ((cg instanceof PCChoiceGenerator) && cg != null) {
		// pc = ((PCChoiceGenerator) cg).getCurrentPC();
		// }
		// return pc;
		// IMPROVED CODE
		ChoiceGenerator<?> cg = vm.getChoiceGenerator();
		while (cg != null) {
			if (cg instanceof PCChoiceGenerator) {
				return ((PCChoiceGenerator) cg).getCurrentPC();
			}
			cg = cg.getPreviousChoiceGenerator();
		}
		return null;
	}

	/**
	 * Given a path condition, calculate the minimal path condition and its
	 * prior probability, and store them in {@link #minimalPC} and
	 * {@link #prior}, respectively.
	 * 
	 * @param pc
	 *            the current path condition
	 */
	private void calcMinPC(PathCondition pc) {
		// calculate the minimal constraints
		Set<Constraint> minConstraints = DependencyCalc.calcMinConstraints(pc);

		// compute the "prior" probability
		PathCondition tmpPC = pc.make_copy();
		tmpPC.removeHeader();
		prior = Apfloat.ONE;
		while (tmpPC.header != null) {
			if (minConstraints.contains(tmpPC.header)) {
				assert conditionalMap.containsKey(tmpPC);
				prior = prior.multiply(conditionalMap.get(tmpPC));
			}
			tmpPC.removeHeader();
		}

		// ok, now we construct the minimal PC
		minimalPC = new PathCondition();
		minimalPC.header = DependencyCalc.copyConstraint(pc.header);
		Constraint c = minimalPC.header;
		for (Constraint d = pc.header.and; d != null; d = d.getTail()) {
			if (minConstraints.contains(d)) {
				c.and = DependencyCalc.copyConstraint(d);
				c = c.and;
			}
		}
		minimalPC.recomputeCount();
		minimalPC.resetHashCode();
		// END comment from here for slicing off
	}

}